Papers with base translator
NL2Lean: Translating Natural Language into Lean 4 through Multi-Aspect Reinforcement Learning (2025.emnlp-main)
Copied to clipboard
Yue Fang, Shaohan Huang, Xin Yu, Haizhen Huang, Zihan Zhang, Weiwei Deng, Furu Wei, Feng Sun, Qi Zhang, Zhi Jin
| Challenge: | Existing formal proof assistants rely on instruction tuning and lack fine-grained structural and semantic alignment. |
| Approach: | They propose a reinforcement learning framework that enables LLMs to translate natural language into formal language such as Lean 4 . they use a model with basic translation ability to refine the model's reinforcement learning . |
| Outcome: | The proposed method outperforms baseline models on NL-to-Lean 4 tasks. |